package alloy.transform.atomize;

import alloy.ast.Variable;
import alloy.semantic.LocalScope;

/**
 * Transient state for the AtomizationVisitor
 * 
 * @author drayside, vshyeung
 * 
 */
class TransientState {

	/** represents the LocalScope of the current state */
	LocalScope _curLocalScope;

	/**
	 * for generating the "a in none" formula when atomization genereates some
	 * bogus quantified formula like <code>some a: A1 | a in A2</code>. This
	 * will become <code>some a: A1 | a in none[a]</code>. We need a
	 * reference for a, which is what this variable is for. Of course, we
	 * could've just put in not {} (the always true EmptyFormula), but that
	 * would be very incomprehensible. However, could it actually be better
	 * performance-wise?
	 */
	Variable _innermostQuantifiedVar;

	String _innermostQuantifiedVarName;

	/**
	 * represents a new LocalScope that needs to be added if VarCreator's are
	 * encountered in the current state
	 */
	LocalScope _localScopeToAdd;

	/**
	 * represents an old LocalScope that needs to be removed if VarCreator's are
	 * encountered in the current state
	 */
	LocalScope _localScopeToRemove;

	TransientState() {
		_localScopeToRemove = null;
		_localScopeToAdd = null;
		_curLocalScope = null;
		_innermostQuantifiedVar = null;
		_innermostQuantifiedVarName = null;
	}
}
